\begin{tabbing}
$\forall$$k$:Knd, $T$,$B$:Type, $l$:IdLnk, ${\it ds}$:fpf(Id; $x$.Type), ${\it tg}$:Id, $f$:(decl{-}state(${\it ds}$)$\rightarrow$$T$$\rightarrow$$B$).
\\[0ex](($\uparrow$isrcv($k$))
\\[0ex]$\Rightarrow$ ((destination(lnk($k$)) = source($l$) $\in$ Id) $\wedge$ ((lnk($k$) = $l$) $\Rightarrow$ (($T$ = $B$) $\wedge$ (tag($k$) = ${\it tg}$)))))
\\[0ex]$\Rightarrow$ normal{-}ds\=\{i:l\}\+
\\[0ex](${\it ds}$)
\-\\[0ex]$\Rightarrow$ normal{-}type\=\{i:l\}\+
\\[0ex]($T$)
\-\\[0ex]$\Rightarrow$ normal{-}type\=\{i:l\}\+
\\[0ex]($B$)
\-\\[0ex]$\Rightarrow$ R{-}realizes\=\{i:l\}\+
\\[0ex](\=Rsends(\=${\it ds}$;\+\+
\\[0ex]$k$;
\\[0ex]$T$;
\\[0ex]$l$;
\\[0ex]fpf{-}single(${\it tg}$; $B$);
\\[0ex]cons($<$${\it tg}$, $\lambda$$s$,$v$. cons(($f$($s$,$v$)); [])$>$; []));
\-\\[0ex]${\it es}$.usends1{-}p(${\it es}$;${\it ds}$;$k$;$T$;$l$;${\it tg}$;$B$;$f$))
\-\-
\end{tabbing}